YES 1.026 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((enumFrom :: Ordering  ->  [Ordering]) :: Ordering  ->  [Ordering])

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((enumFrom :: Ordering  ->  [Ordering]) :: Ordering  ->  [Ordering])

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
takeWhile p [] = []
takeWhile p (x : xs)
 | p x
 = x : takeWhile p xs
 | otherwise
 = []

is transformed to
takeWhile p [] = takeWhile3 p []
takeWhile p (x : xs) = takeWhile2 p (x : xs)

takeWhile1 p x xs True = x : takeWhile p xs
takeWhile1 p x xs False = takeWhile0 p x xs otherwise

takeWhile0 p x xs True = []

takeWhile2 p (x : xs) = takeWhile1 p x xs (p x)

takeWhile3 p [] = []
takeWhile3 wv ww = takeWhile2 wv ww

The following Function with conditions
toEnum 0 = LT
toEnum 1 = EQ
toEnum 2 = GT

is transformed to
toEnum xw = toEnum5 xw
toEnum wy = toEnum3 wy
toEnum wx = toEnum1 wx

toEnum0 True wx = GT

toEnum1 wx = toEnum0 (wx == 2) wx

toEnum2 True wy = EQ
toEnum2 wz xu = toEnum1 xu

toEnum3 wy = toEnum2 (wy == 1) wy
toEnum3 xv = toEnum1 xv

toEnum4 True xw = LT
toEnum4 xx xy = toEnum3 xy

toEnum5 xw = toEnum4 (xw == 0) xw
toEnum5 xz = toEnum3 xz



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ NumRed

mainModule Main
  ((enumFrom :: Ordering  ->  [Ordering]) :: Ordering  ->  [Ordering])

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ NumRed
HASKELL
              ↳ Narrow

mainModule Main
  (enumFrom :: Ordering  ->  [Ordering])

module Main where
  import qualified Prelude



Haskell To QDPs